w_locle(w;x;y) == x ((x,y. first(y) & x = pred(y))^*) y 

latex

---

clarification:

w_locle(w;x;y)
== x rel_star(w-E(w);(x,y. first(e.w-pred(w;e);y) & x = pred(e.w-pred(w;e);y)  w-E(w))) y 

latex

Definitions	x f y, R^*, A & B, A, b, first(e), s = t, E, pred(e), x.A(x), w-pred(w;e)
FDL editor aliases	w_locle